Presently  there are no automatic, nor machine-assisted, tools for the simulation and verification of concurrent systems specified in \ntcc. Since we deal with complex and large systems, these tools are essential to our intended applications. 
%This issue  has hitherto been far too little considered for \ccp\ formalisms. 
In fact, the issue of automatic support has received little attention in the case of \ccp formalisms. To our knowledge only Villanueva et al (e.g. \cite{AGPV06,FalaschiV06}) have addressed automatic verification but in the context of finite-state \ccp systems. Several applications of \ntcc are, however, inherently infinite-state. Automatic verification of large systems, not to mention infinite systems, is challenging because of the state explosion problem it poses---i.e., the number of states a system has is exponential in the number of  processes.  

We will take up this challenge  by identifying \ntcc\  fragments amenable to  automatic verification and by developing  techniques and tools to machine assist the verification of system properties in \ntcc. We envisage two main complementary approaches for our purposes:  (1) Automaton-based and symbolic techniques,  and (2) Static and abstract interpretation techniques.  We plan to use the automaton representations of processes used to prove the the decidability of the verification problem for \ntcc \cite{Valencia05},  together with the symbolic approach in \cite{Olarte:08:SAC}  to ameliorate the state explosion problem. Finally, we expect to develop static and abstract interpretation techniques to extract representative information from system specifications. Such information can be used to reason about essential properties of systems behavior. 

We plan to use Security Protocols to test the above-mentioned  techniques and tools. In fact, the analysis of Security Protocols is typically carried out using symbolic verification techniques thus making them  ideal application candidates. It is also worth noticing that computer simulation plays a fundamental role for Biological Systems because of their inherent complexity. We also plan to develop an \ntcc simulation tool and use it as a test bench for (abstractions of) biological systems.  We expect that the declarative and parametric nature of \ntcc should provide bench biologists with a tool for computing with and analyzing these systems that is intuitive.